(SETQ SETQMESS @("
No proof has been found.  You have two options:
1)Type AB <clauses>; to abandon the current proof attempt, retaining
  <clauses> for the clause list.
2)Type TE <clauses>; to terminate this attempt, but then automatically
 begin a new search with <clauses> added to the set of initial statements.

You are now talking to the on-line editor... for help type HE; 
"))
(SETQ MESSAGE @("
Help-message is under revision.  Read PROVER.DOC[P,JRA].More document-
ation is coming.
As a last resort call 321-3612.
"))